Specializations of ANYTHING include:

S-I.	ANYTHING [NAME PRINT-NAME]

S-II.	CON-TYPE [EXAMPLES GENL SPECL]
	Anything that can have an EXAMPLES facet isa CON-TYPE.
	This implies that any specialization of an example of
	CON-TYPE is also an example of CON-TYPE.
	High-level examples of CON-TYPE include:
	E-A.	ANYTHING
	E-B.	CON-TYPE
	E-C.	CONSTRUCTOR
	E-D.	FACET-TYPE
	E-E.	HEURISTIC
	E-F.	OBJECT
	E-G.	JUSTIFICATION
	E-H.	PROPOSITION
	E-I.	TYPICAL-ELEM
	E-J.	TYPICAL-EXAMPLE
	The examples of CON-TYPE are precisely the SPECIALIZATIONS of
	ANYTHING.  The items listed above are considered in more
	detail under that heading.
	An important specialization of CON-TYPE is:
	S-A.	ONE-ARG-PRED

S-III.	CONSTRUCTOR
	Anything that can appear just after a '(' in a definition is a
	CONSTRUCTOR.  Intuitively a constructor is a function which
	operates on one or more concepts to construct a new concept.
	CONSTRUCTORs are classified according to the kinds of concepts
	they operate on and the kinds of concepts they produce.
	High-level specializations of CONSTRUCTOR include:
	S-A.	CONNECTIVE
		A CONNECTIVE operates on PROPOSITIONs to construct a
		PROPOSITION.
		Examples of CONNECTIVE include:
		e-1.	AND
		e-2.	IFF
		e-3.	IMPLIES
		e-4.	NOT
		e-5.	OR
		e-6.	XOR
		with the usual meanings.
	S-B.	OPERATION
		An OPERATION operates on OBJECTs to produce an OBJECT.
		Examples of OPERATION include:
		e-1.	INTERSECTION
			INTERSECTION operates on two CLASSes, X and Y,
			to construct the CLASS of all ELEMENTs which
			are ELEMs of both X and Y.
		e-2.	ORDERED-PAIR
			ORDERED-PAIR operates on two ELEMENTs, X and Y,
			to construct the ordered-pair, (X,Y), which is
			an EXAMPLE of IS-ORDERED-PAIR.
		e-3.	VALUE-AT
			VALUE-AT operates on a FUNCTION, F, and an
			ELEMENT, X, to produce the unique ELEMENT, Y,
			such that (X,Y) is an ELEM of F.  If there is
			no such Y, or if there are more than one, then
			(VALUE-AT F X) is undefined.
		e-4.	IMAGE
			IMAGE operates on a RELATION, R, and a CLASS,
			C, to produce the class of all ELEMENTs, Y,
			such that (X,Y) is in R for some X.
	S-C.	PREDICATE
		A PREDICATE operates on OBJECTS to construct a
		PROPOSITION.
		Some important specializations of PREDICATE are:
		s-1.	ONE-ARG-PRED
			A ONE-ARG-PRED is a PREDICATE which operates
			on a single OBJECT.  A ONE-ARG-PRED, P, is
			identified with the concept of "OBJECTs which
			satisfy P" (where an OBJECT, X, "satisfies" P
			iff the PROPOSITION constructed when P operates
			on X is a true PROPOSITION).
			The examples of ONE-ARG-PRED are precisely the
			specializations of OBJECT.
		s-2.	TWO-ARG-PRED
			A TWO-ARG-PRED is a PREDICATE which operates
			on two OBJECTs.  A TWO-ARG-PRED, P, is identi-
			fied with the FACET-TYPE, *P, such that the
			items on the *P facet of an OBJECT, X, are
			those objects, Y, such that the PROPOSITION
			(P Y X) is true.
		Some examples of PREDICATE (other than examples of
		ONE-ARG-PRED and TWO-ARG-PRED) are:
		e-1.	MAPS-INTO
			Let F be a FUNCTION and let X and Y be
			CLASSes.  Then (MAPS-INTO F X Y), read "F
			maps X into Y, holds iff the domain of F is
			X and the range of F is a subset of Y.
		e-2.	POINT-IDENTITY-UNDER
			Let * be a binary operation (BIN-OP), and let
			S and E be ELEMENTs.  Then, (POINT-IDENTITY-
			UNDER E S *), read "E is an identity of S
			under *", holds iff E and S are in the "domain"
			(actually the OP-DOMAIN) of * and E*S = S*E =
			S.  Thus, E is an identity of * iff (POINT-
			IDENTITY-UNDER E X *) holds for every X in
			the OP-DOMAIN of *.
		e-3.	RELATED
			Let R be a RELATION, and let X and Y be
			ELEMENTs.  Then, the PROPOSITION, (RELATED
			X R Y), read "X is related to Y under R", holds
			iff (ELEM (ORDERED-PAIR X Y) R) holds.
		e-4.	VECTOR-SPACE-OVER-UNDER
			Suppose that F is a FIELD, that V is a CLASS,
			that Plus is a binary operation on V, and that
			Times is FUNCTION on the cross product of
			(the underlying set of F) with V.  Then,
			(VECTOR-SPACE-OVER-UNDER V F Plus Times), read
			"V is a vector space over F under vector
			addition, Plus, and mixed multiplication,
			Times", iff V, F, Plus, and Times satisfy the
			vector space axioms (which I won't bother to
			list here).
	S-D.	QUANTIFIER
******* P U N T *******
		Examples of QUANTIFIER include:
		e-1.	EX-UNIQ
		e-2.	EXISTS
		e-3.	EXISTS\ELEMENT
		e-4.	FORALL
		e-5.	FORALL-IN
******* ALL   P U N T E D *******
	S-E.	SPECIFIER
******* P U N T *******
		e-1.	CLASS-OF
		e-2.	CLASS-OF-FORM
		e-3.	UNIQ
******* ALL   P U N T E D *******

S-IV.	FACET-TYPE [CON-DOMAIN CON-RANGE]
	Examples of FACET-TYPE include:
	E-A.	ISA
	E-B.	FACETS
		Let CON be a concept, and let FAC be a facet.  Then,
		the FACETS facet of the concept CON:ANY-FAC has on it
		those FACET-TYPEs, TYP, such that it is meaningful
		to speak of the TYP facet of any concept on the FAC
		facet of CON.  For example, if the CARD facet is
		defined in such a way that for any CLASS, C, (i.e.,
		for any concept, C, which is an EXAMPLE of CLASS) the
		CARD facet of C contains the cardinality of C, then
		CLASS:ANY-EXAMPLE will have CARD on its FACETS facet.
	E-C.	ARGUMENTS
		The ARGUMENTS facet of any CONSTRUCTOR, CON, is a list
		which tells what kinds of OBJECTs CON operates on and
		gives those objects formal names which are used in the
		DEFININTION, STATEMENT, or VALUE facet of CON.  For
		example, the CONSTRUCTOR, RELATED (See S-III:S-C:e-3),
		has as its ARGUMENTS facet:
		    (ARGUMENTS (X ELEMENT) (R RELATION) (Y ELEMENT)),
		indicating that the items on which it operates must be,
		in order, an ELEMENT, a RELATION, and another ELEMENT,
		and further indicating that these items are referred
		to a X, R, Y, respectively in its DEFINITION facet:
		    (DEFINITION (ELEM (ORDERED-PAIR X Y) R)).
	E-D.	ARG-TYPES
		For any specialization, SCON, of CONSTRUCTOR, the
		ARG-TYPES facet of SCON has on it the possible
		CON-TYPEs on whose EXAMPLEs the EXAMPLEs of SCON
		may operate.  Consider, for example, the speciali-
		zation, OPERATION, of CONSTRUCTOR.  The items
		operated on by EXAMPLEs of OPERATION (e.g., IMAGE)
		must be EXAMPLEs of OBJECT (e.g., the sine function
		and the class of all real numbers in the interval
		[0,pi]).  Thus, for the ARG-TYPES facet of OPERATION
		we have:
		    (ARG-TYPES OBJECT).
		A QUANTIFIER, on the other hand, can operate on
		objects, variables, and propositions (consider, for
		example, EXISTS-IN).  Thus, for the ARG-TYPES facet
		of QUANTIFIER we have
		    (ARG-TYPES VARIABLE OBJECT PROPOSITION).
	E-E.	PRODUCES
		For any specialization, SCON, of CONSTRUCTOR, the
		PRODUCES facet of SCON has on it the possible
		CON-TYPEs of which EXAMPLEs may be constructed by the
		EXAMPLEs of SCON.  Consider, for example, the speciali-
		zation, OPERATION, of CONSTRUCTOR.  The items
		constructed by EXAMPLEs of OPERATION (e.g., IMAGE)
		must be EXAMPLEs of OBJECT (e.g., the class of all real
		numbers in the interval [0,1]).  Thus, for the PRODUCES
		facet of OPERATION we have:
		    (PRODUCES OBJECT).
		A QUANTIFIER, on the other hand, always constructs a
		proposition.  Thus, for the PRODUCES facet of
		QUANTIFIER we have
		    (PRODUCES PROPOSITION).
	E-F.	NAME
	E-G.	PRINT-NAME
******* TEMPORARILY   P U N T E D *******
	E-H.	DEFINITION
		Let BUILD be a CONNECTIVE, QUANTIFIER, PREDICATE, or
		SPECIFIER (thus, BUILD will be a CONSTRUCTOR).  Then,
		the DEFINITION facet of BUILD will contain an
		expression describing the item constructed by BUILD
		in terms of the items on which BUILD operates.  For
		an example, see S-IV:E-C.
	E-I.	STATEMENT
		The STATEMENT facet of a PROPOSITION is a formal
		expression which asserts that PROPOSITION.  As an
		example, the THEOREM, UNICITY-OF-TWO-SIDED-IDENTITY,
		has as its STATEMENT facet:
		    (STATEMENT (IMPLIES (AND (IDENTITY-OF E1 STAR)
					     (IDENTITY-OF E2 STAR))
					(EQUALS E1 E2)))
	E-J.	VALUE
		The VALUE facet of an OBJECT is a formal expression
		denoting that OBJECT, and the VALUE facet of an
		OPERATION holds a formal expression denoting the OBJECT
		constructed by that operation, in terms of the OBJECTs
		on which it operates (as specified in the ARGUMENTS
		facet).  For example, the OPERATION, IMAGE (see S-III:
		S-B:e-4), operates on two OBJECTs, R and C, which must
		be EXAMPLEs of RELATION and CLASS, respectively, as
		indicated in IMAGE's ARGUMENTS facet:
		    (ARGUMENTS (R RELATION) (C CLASS)),
		and produces an OBJECT, the image of R under C, as
		defined by IMAGE's VALUE facet:
		    (VALUE (CLASS-OF Y
				     (EXISTS X
					     (AND (ELEM X C)
						  (RELATED X R Y)))))
	E-K.	ENGLISH
		This facet contains an English language version of
		a concept's STATEMENT, DEFINITION, or VALUE facet.
		As the ENGLISH facet of the THEOREM, UNICITY-OF-
		TWO-SIDED-IDENTITY, for example, we might have:
		    (ENGLISH "A binary operation can have at most o↑Y
		    ne identity.").
	E-L.	COMMENTS
		This facet is used to hold useful English language
		information about a concept which does not belong on
		the ENGLISH facet because it is not semantically
		equivalent to the STATEMENT, DEFINITION, or VALUE
		facet.
	E-M.	GENL
	E-N.	SPECL
	E-O.	EXAMPLES
	E-P.	ELEMS
		The ELEMS facet of a CLASS, C, contains ELEMENTS which
		are elements of C (i.e., ELEMENTS, X, such that the
		PROPOSITION, (ELEM X C), holds).
	E-Q.	ISIN
		This facet is the inverse of the ELEMS facet.
	E-R.	THMS
		The THMS facet of a concept, CON, points to THEOREMs
		which deal with CON.
	E-S.	HEURISTICS
		The HEURISTICS facet of a concept, CON, points to
		HEURISTICs which are applicable to investigations
		involving CON.
	E-T.	CON-DOMAIN
		Let FAC be a FACET-TYPE, and let CONT be a CON-TYPE.
		Then CONT is on the CON-DOMAIN facet of FAC iff all
		EXAMPLEs of CONT may meaningfully have FAC facets.  For
		example, every EXAMPLE of CONSTRUCTOR (e.g., IMPLIES,
		IMAGE, RELATED) has an ARGUMENTS facet, and only
		CONSTRUCTORs may have ARGUMENTS facets.  Thus, for the
		CON-DOMAIN facet of ARGUMENTS, we have:
		    (CON-DOMAIN CONSTRUCTOR)
		As another example, both OBJECTs and OPERATIONs may
		have VALUE facets.  Thus, for the CON-DOMAIN facet of
		VALUE we have:
		    (CON-DOMAIN OBJECT OPERATION).
		In this outline, each FACET-TYPE appears in square
		brackets after the headings for the CON-TYPES on its
		CON-DOMAIN facet.
	E-U.	CON-RANGE
		The CON-RANGE facet of a FACET-TYPE, FAC, contains
		those CON-TYPEs whose EXAMPLEs might legitimately
		occur on the FAC facet of some concept.  For example,
		anything on the THMS facet of a concept must be a
		THEOREM.  Thus, for the CON-RANGE facet of THMS we
		have:
		    (CON-RANGE THEOREM).

S-V.	HEURISTIC

S-VI.	OBJECT
	OBJECTs are the nouns of mathematical sentences.  The
	QUANTIFIERs, FORALL and EXISTS, quantify over OBJECTs.
	High-level specializations of OBJECT include:
	S-A	ATOM
		An ATOM is a mathematical object which is considered
		to be primitive in that no ATOM may have any OBJECT as
		an element.
	S-B.	CLASS
		A CLASS is an OBJECT which is considered to be a
		collection (possibly empty) of OBJECTs (which may
		be ATOMs or CLASSes).
		Two important specializations of CLASS are:
		s-1.	SET
			A SET is any CLASS which is an element of a
			CLASS.  In other words, a CLASS, X, is a SET
			iff there is some CLASS, Y, such that the
			PROPOSITION, (ELEM X Y), holds.  Most of the
			CLASSes with which we ordinarily deal in
			mathematics are, in fact, SETs.
			Examples of SET include:
			e-a.	PHI
				PHI is the empty CLASS.  PHI is the
				CLASS which has no elements (ELEMSs).
				An OBJECT, OB, has no elements iff
				OB is PHI or OB is an ATOM.
			e-b.	THE-REALS
				This is the SET whose elements are
				precisely the real numbers.
				SUBCLASSes of THE-REALS include:
				sc-i.	THE-POSITIVE-REALS
				sc-ii.	THE-RATIONALS
				sc-iii.	THE-INTEGERS
				sc-iv.	THE-PRIMES
				sc-v.	THE-PERFECT-SQUARES
			e-c.	OMEGA
				OMEGA is the first infinite ordinal.
		s-2.	PROPER-CLASS
			The PROPER-CLASSes are those CLASSes which are
			not SETs.  Intuitively, a PROPER-CLASS is a
			CLASS which is too big to be an element (ELEM)
			of any CLASS.
			Examples of PROPER-CLASS include:
			e-a.	UNIVERSE
				This CLASS has every SET and ATOM as an
				element.
			e-b.	THE-ORDINALS
				This CLASS has as its elements all
				ORDINALs which are SETs.
ANYTHING
S-I.	ANYTHING [NAME PRINT-NAME]
S-II.	CON-TYPE [EXAMPLES GENL SPECL]
	E-A.	ANYTHING
	E-B.	CON-TYPE
	E-C.	CONSTRUCTOR
	E-D.	FACET-TYPE
	E-E.	HEURISTIC
	E-F.	OBJECT
	E-G.	JUSTIFICATION
	E-H.	PROPOSITION
	E-I.	TYPICAL-ELEM
	E-J.	TYPICAL-EXAMPLE
	S-A.	ONE-ARG-PRED
S-III.	CONSTRUCTOR
	S-A.	CONNECTIVE
		e-1.	AND
		e-2.	IFF
		e-3.	IMPLIES
		e-4.	NOT
		e-5.	OR
		e-6.	XOR
	S-B.	OPERATION
		e-1.	INTERSECTION
		e-2.	ORDERED-PAIR
		e-3.	VALUE-AT
		e-4.	IMAGE
	S-C.	PREDICATE
		s-1.	ONE-ARG-PRED
		s-2.	TWO-ARG-PRED
		e-1.	MAPS-INTO
		e-2.	POINT-IDENTITY-UNDER
		e-3.	RELATED
		e-4.	VECTOR-SPACE-OVER-UNDER
	S-D.	QUANTIFIER
		e-1.	EX-UNIQ
		e-2.	EXISTS
		e-3.	EXISTS\ELEMENT
		e-4.	FORALL
		e-5.	FORALL-IN
	S-E.	SPECIFIER
		e-1.	CLASS-OF
		e-2.	CLASS-OF-FORM
		e-3.	UNIQ
S-IV.	FACET-TYPE [CON-DOMAIN CON-RANGE]
	E-A.	ISA
	E-B.	FACETS
	E-C.	ARGUMENTS
	E-D.	ARG-TYPES
	E-E.	PRODUCES
	E-F.	NAME
	E-G.	PRINT-NAME
	E-H.	DEFINITION
	E-I.	STATEMENT
	E-J.	VALUE
	E-K.	ENGLISH
	E-L.	COMMENTS
	E-M.	GENL
	E-N.	SPECL
	E-O.	EXAMPLES
	E-P.	ELEMS
	E-Q.	ISIN
	E-R.	THMS
	E-S.	HEURISTICS
	E-T.	CON-DOMAIN
	E-U.	CON-RANGE
S-V.	HEURISTIC
S-VI.	OBJECT
	S-A	ATOM
	S-B.	CLASS
		s-1.	SET
			e-a.	PHI
			e-b.	THE-REALS
				sc-i.	THE-POSITIVE-REALS
				sc-ii.	THE-RATIONALS
				sc-iii.	THE-INTEGERS
				sc-iv.	THE-PRIMES
				sc-v.	THE-PERFECT-SQUARES
			e-c.	OMEGA
		s-2.	PROPER-CLASS
			e-a.	UNIVERSE
			e-b.	THE-ORDINALS